MAYBE 20.903 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could not be shown:



HASKELL
  ↳ BR

mainModule Main
  ((enumFromThenTo :: Int  ->  Int  ->  Int  ->  [Int]) :: Int  ->  Int  ->  Int  ->  [Int])

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule Main
  ((enumFromThenTo :: Int  ->  Int  ->  Int  ->  [Int]) :: Int  ->  Int  ->  Int  ->  [Int])

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False

The following Function with conditions
p 
 | n' >= n
 = flip (<=) m
 | otherwise
 = flip (>=) m

is transformed to
p  = p2

p0 True = flip (>=) m

p1 True = flip (<=) m
p1 False = p0 otherwise

p2  = p1 (n' >= n)

The following Function with conditions
takeWhile p [] = []
takeWhile p (x : xs)
 | p x
 = x : takeWhile p xs
 | otherwise
 = []

is transformed to
takeWhile p [] = takeWhile3 p []
takeWhile p (x : xs) = takeWhile2 p (x : xs)

takeWhile0 p x xs True = []

takeWhile1 p x xs True = x : takeWhile p xs
takeWhile1 p x xs False = takeWhile0 p x xs otherwise

takeWhile2 p (x : xs) = takeWhile1 p x xs (p x)

takeWhile3 p [] = []
takeWhile3 vz wu = takeWhile2 vz wu



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ LetRed

mainModule Main
  ((enumFromThenTo :: Int  ->  Int  ->  Int  ->  [Int]) :: Int  ->  Int  ->  Int  ->  [Int])

module Main where
  import qualified Prelude



Let/Where Reductions:
The bindings of the following Let/Where expression
takeWhile p (numericEnumFromThen n n')
where 
p  = p2
p0 True = flip (>=) m
p1 True = flip (<=) m
p1 False = p0 otherwise
p2  = p1 (n' >= n)

are unpacked to the following functions on top level
numericEnumFromThenToP0 wv ww wx True = flip (>=) wv

numericEnumFromThenToP1 wv ww wx True = flip (<=) wv
numericEnumFromThenToP1 wv ww wx False = numericEnumFromThenToP0 wv ww wx otherwise

numericEnumFromThenToP wv ww wx = numericEnumFromThenToP2 wv ww wx

numericEnumFromThenToP2 wv ww wx = numericEnumFromThenToP1 wv ww wx (ww >= wx)



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
HASKELL
              ↳ Narrow
              ↳ Narrow

mainModule Main
  (enumFromThenTo :: Int  ->  Int  ->  Int  ->  [Int])

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNat(Succ(wy9200), Succ(wy3900)) → new_primMinusNat(wy9200, wy3900)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(wy9200), Succ(wy3900)) → new_primPlusNat(wy9200, wy3900)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ Rewriting
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_iterate(wy165, wy164, wy163) → new_iterate(wy165, wy165, new_ps(wy164, wy163))

The TRS R consists of the following rules:

new_primPlusNat0(Zero, Zero) → Zero
new_primPlusInt(Pos(wy920), Pos(wy390)) → Pos(new_primPlusNat0(wy920, wy390))
new_primMinusNat0(Zero, Zero) → Pos(Zero)
new_primPlusInt(Neg(wy920), Neg(wy390)) → Neg(new_primPlusNat0(wy920, wy390))
new_primMinusNat0(Succ(wy9200), Zero) → Pos(Succ(wy9200))
new_primMinusNat0(Zero, Succ(wy3900)) → Neg(Succ(wy3900))
new_primPlusNat0(Zero, Succ(wy3900)) → Succ(wy3900)
new_primPlusNat0(Succ(wy9200), Zero) → Succ(wy9200)
new_primPlusNat0(Succ(wy9200), Succ(wy3900)) → Succ(Succ(new_primPlusNat0(wy9200, wy3900)))
new_ps(wy164, wy163) → new_primPlusInt(wy164, wy163)
new_primPlusInt(Neg(wy920), Pos(wy390)) → new_primMinusNat0(wy390, wy920)
new_primPlusInt(Pos(wy920), Neg(wy390)) → new_primMinusNat0(wy920, wy390)
new_primMinusNat0(Succ(wy9200), Succ(wy3900)) → new_primMinusNat0(wy9200, wy3900)

The set Q consists of the following terms:

new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_ps(x0, x1)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusInt(Pos(x0), Neg(x1))
new_primPlusInt(Neg(x0), Pos(x1))
new_primPlusNat0(Zero, Zero)
new_primMinusNat0(Zero, Zero)
new_primMinusNat0(Zero, Succ(x0))
new_primPlusInt(Neg(x0), Neg(x1))
new_primMinusNat0(Succ(x0), Zero)
new_primPlusInt(Pos(x0), Pos(x1))
new_primMinusNat0(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_iterate(wy165, wy164, wy163) → new_iterate(wy165, wy165, new_ps(wy164, wy163)) at position [2] we obtained the following new rules:

new_iterate(wy165, wy164, wy163) → new_iterate(wy165, wy165, new_primPlusInt(wy164, wy163))



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ Rewriting
QDP
                        ↳ UsableRulesProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_iterate(wy165, wy164, wy163) → new_iterate(wy165, wy165, new_primPlusInt(wy164, wy163))

The TRS R consists of the following rules:

new_primPlusNat0(Zero, Zero) → Zero
new_primPlusInt(Pos(wy920), Pos(wy390)) → Pos(new_primPlusNat0(wy920, wy390))
new_primMinusNat0(Zero, Zero) → Pos(Zero)
new_primPlusInt(Neg(wy920), Neg(wy390)) → Neg(new_primPlusNat0(wy920, wy390))
new_primMinusNat0(Succ(wy9200), Zero) → Pos(Succ(wy9200))
new_primMinusNat0(Zero, Succ(wy3900)) → Neg(Succ(wy3900))
new_primPlusNat0(Zero, Succ(wy3900)) → Succ(wy3900)
new_primPlusNat0(Succ(wy9200), Zero) → Succ(wy9200)
new_primPlusNat0(Succ(wy9200), Succ(wy3900)) → Succ(Succ(new_primPlusNat0(wy9200, wy3900)))
new_ps(wy164, wy163) → new_primPlusInt(wy164, wy163)
new_primPlusInt(Neg(wy920), Pos(wy390)) → new_primMinusNat0(wy390, wy920)
new_primPlusInt(Pos(wy920), Neg(wy390)) → new_primMinusNat0(wy920, wy390)
new_primMinusNat0(Succ(wy9200), Succ(wy3900)) → new_primMinusNat0(wy9200, wy3900)

The set Q consists of the following terms:

new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_ps(x0, x1)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusInt(Pos(x0), Neg(x1))
new_primPlusInt(Neg(x0), Pos(x1))
new_primPlusNat0(Zero, Zero)
new_primMinusNat0(Zero, Zero)
new_primMinusNat0(Zero, Succ(x0))
new_primPlusInt(Neg(x0), Neg(x1))
new_primMinusNat0(Succ(x0), Zero)
new_primPlusInt(Pos(x0), Pos(x1))
new_primMinusNat0(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ Rewriting
                      ↳ QDP
                        ↳ UsableRulesProof
QDP
                            ↳ QReductionProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_iterate(wy165, wy164, wy163) → new_iterate(wy165, wy165, new_primPlusInt(wy164, wy163))

The TRS R consists of the following rules:

new_primPlusInt(Pos(wy920), Pos(wy390)) → Pos(new_primPlusNat0(wy920, wy390))
new_primPlusInt(Neg(wy920), Neg(wy390)) → Neg(new_primPlusNat0(wy920, wy390))
new_primPlusInt(Neg(wy920), Pos(wy390)) → new_primMinusNat0(wy390, wy920)
new_primPlusInt(Pos(wy920), Neg(wy390)) → new_primMinusNat0(wy920, wy390)
new_primMinusNat0(Zero, Zero) → Pos(Zero)
new_primMinusNat0(Succ(wy9200), Zero) → Pos(Succ(wy9200))
new_primMinusNat0(Zero, Succ(wy3900)) → Neg(Succ(wy3900))
new_primMinusNat0(Succ(wy9200), Succ(wy3900)) → new_primMinusNat0(wy9200, wy3900)
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Zero, Succ(wy3900)) → Succ(wy3900)
new_primPlusNat0(Succ(wy9200), Zero) → Succ(wy9200)
new_primPlusNat0(Succ(wy9200), Succ(wy3900)) → Succ(Succ(new_primPlusNat0(wy9200, wy3900)))

The set Q consists of the following terms:

new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_ps(x0, x1)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusInt(Pos(x0), Neg(x1))
new_primPlusInt(Neg(x0), Pos(x1))
new_primPlusNat0(Zero, Zero)
new_primMinusNat0(Zero, Zero)
new_primMinusNat0(Zero, Succ(x0))
new_primPlusInt(Neg(x0), Neg(x1))
new_primMinusNat0(Succ(x0), Zero)
new_primPlusInt(Pos(x0), Pos(x1))
new_primMinusNat0(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_ps(x0, x1)



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ Rewriting
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ QReductionProof
QDP
                                ↳ Instantiation
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_iterate(wy165, wy164, wy163) → new_iterate(wy165, wy165, new_primPlusInt(wy164, wy163))

The TRS R consists of the following rules:

new_primPlusInt(Pos(wy920), Pos(wy390)) → Pos(new_primPlusNat0(wy920, wy390))
new_primPlusInt(Neg(wy920), Neg(wy390)) → Neg(new_primPlusNat0(wy920, wy390))
new_primPlusInt(Neg(wy920), Pos(wy390)) → new_primMinusNat0(wy390, wy920)
new_primPlusInt(Pos(wy920), Neg(wy390)) → new_primMinusNat0(wy920, wy390)
new_primMinusNat0(Zero, Zero) → Pos(Zero)
new_primMinusNat0(Succ(wy9200), Zero) → Pos(Succ(wy9200))
new_primMinusNat0(Zero, Succ(wy3900)) → Neg(Succ(wy3900))
new_primMinusNat0(Succ(wy9200), Succ(wy3900)) → new_primMinusNat0(wy9200, wy3900)
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Zero, Succ(wy3900)) → Succ(wy3900)
new_primPlusNat0(Succ(wy9200), Zero) → Succ(wy9200)
new_primPlusNat0(Succ(wy9200), Succ(wy3900)) → Succ(Succ(new_primPlusNat0(wy9200, wy3900)))

The set Q consists of the following terms:

new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusInt(Pos(x0), Neg(x1))
new_primPlusInt(Neg(x0), Pos(x1))
new_primPlusNat0(Zero, Zero)
new_primMinusNat0(Zero, Zero)
new_primMinusNat0(Zero, Succ(x0))
new_primPlusInt(Neg(x0), Neg(x1))
new_primMinusNat0(Succ(x0), Zero)
new_primPlusInt(Pos(x0), Pos(x1))
new_primMinusNat0(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule new_iterate(wy165, wy164, wy163) → new_iterate(wy165, wy165, new_primPlusInt(wy164, wy163)) we obtained the following new rules:

new_iterate(z0, z0, y_0) → new_iterate(z0, z0, new_primPlusInt(z0, y_0))



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ Rewriting
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ QReductionProof
                              ↳ QDP
                                ↳ Instantiation
QDP
                                    ↳ MNOCProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_iterate(z0, z0, y_0) → new_iterate(z0, z0, new_primPlusInt(z0, y_0))

The TRS R consists of the following rules:

new_primPlusInt(Pos(wy920), Pos(wy390)) → Pos(new_primPlusNat0(wy920, wy390))
new_primPlusInt(Neg(wy920), Neg(wy390)) → Neg(new_primPlusNat0(wy920, wy390))
new_primPlusInt(Neg(wy920), Pos(wy390)) → new_primMinusNat0(wy390, wy920)
new_primPlusInt(Pos(wy920), Neg(wy390)) → new_primMinusNat0(wy920, wy390)
new_primMinusNat0(Zero, Zero) → Pos(Zero)
new_primMinusNat0(Succ(wy9200), Zero) → Pos(Succ(wy9200))
new_primMinusNat0(Zero, Succ(wy3900)) → Neg(Succ(wy3900))
new_primMinusNat0(Succ(wy9200), Succ(wy3900)) → new_primMinusNat0(wy9200, wy3900)
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Zero, Succ(wy3900)) → Succ(wy3900)
new_primPlusNat0(Succ(wy9200), Zero) → Succ(wy9200)
new_primPlusNat0(Succ(wy9200), Succ(wy3900)) → Succ(Succ(new_primPlusNat0(wy9200, wy3900)))

The set Q consists of the following terms:

new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusInt(Pos(x0), Neg(x1))
new_primPlusInt(Neg(x0), Pos(x1))
new_primPlusNat0(Zero, Zero)
new_primMinusNat0(Zero, Zero)
new_primMinusNat0(Zero, Succ(x0))
new_primPlusInt(Neg(x0), Neg(x1))
new_primMinusNat0(Succ(x0), Zero)
new_primPlusInt(Pos(x0), Pos(x1))
new_primMinusNat0(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
We use the modular non-overlap check [17] to decrease Q to the empty set.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ Rewriting
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ QReductionProof
                              ↳ QDP
                                ↳ Instantiation
                                  ↳ QDP
                                    ↳ MNOCProof
QDP
                                        ↳ NonTerminationProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_iterate(z0, z0, y_0) → new_iterate(z0, z0, new_primPlusInt(z0, y_0))

The TRS R consists of the following rules:

new_primPlusInt(Pos(wy920), Pos(wy390)) → Pos(new_primPlusNat0(wy920, wy390))
new_primPlusInt(Neg(wy920), Neg(wy390)) → Neg(new_primPlusNat0(wy920, wy390))
new_primPlusInt(Neg(wy920), Pos(wy390)) → new_primMinusNat0(wy390, wy920)
new_primPlusInt(Pos(wy920), Neg(wy390)) → new_primMinusNat0(wy920, wy390)
new_primMinusNat0(Zero, Zero) → Pos(Zero)
new_primMinusNat0(Succ(wy9200), Zero) → Pos(Succ(wy9200))
new_primMinusNat0(Zero, Succ(wy3900)) → Neg(Succ(wy3900))
new_primMinusNat0(Succ(wy9200), Succ(wy3900)) → new_primMinusNat0(wy9200, wy3900)
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Zero, Succ(wy3900)) → Succ(wy3900)
new_primPlusNat0(Succ(wy9200), Zero) → Succ(wy9200)
new_primPlusNat0(Succ(wy9200), Succ(wy3900)) → Succ(Succ(new_primPlusNat0(wy9200, wy3900)))

Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

new_iterate(z0, z0, y_0) → new_iterate(z0, z0, new_primPlusInt(z0, y_0))

The TRS R consists of the following rules:

new_primPlusInt(Pos(wy920), Pos(wy390)) → Pos(new_primPlusNat0(wy920, wy390))
new_primPlusInt(Neg(wy920), Neg(wy390)) → Neg(new_primPlusNat0(wy920, wy390))
new_primPlusInt(Neg(wy920), Pos(wy390)) → new_primMinusNat0(wy390, wy920)
new_primPlusInt(Pos(wy920), Neg(wy390)) → new_primMinusNat0(wy920, wy390)
new_primMinusNat0(Zero, Zero) → Pos(Zero)
new_primMinusNat0(Succ(wy9200), Zero) → Pos(Succ(wy9200))
new_primMinusNat0(Zero, Succ(wy3900)) → Neg(Succ(wy3900))
new_primMinusNat0(Succ(wy9200), Succ(wy3900)) → new_primMinusNat0(wy9200, wy3900)
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Zero, Succ(wy3900)) → Succ(wy3900)
new_primPlusNat0(Succ(wy9200), Zero) → Succ(wy9200)
new_primPlusNat0(Succ(wy9200), Succ(wy3900)) → Succ(Succ(new_primPlusNat0(wy9200, wy3900)))


s = new_iterate(z0, z0, y_0) evaluates to t =new_iterate(z0, z0, new_primPlusInt(z0, y_0))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:




Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from new_iterate(z0, z0, y_0) to new_iterate(z0, z0, new_primPlusInt(z0, y_0)).





↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile10(wy2180, wy220, wy223) → new_takeWhile1(wy2180, Pos(Succ(wy220)), wy223)
new_takeWhile13(wy361, wy362, wy363, Zero, Zero) → new_takeWhile14(wy361, wy362, wy363)
new_takeWhile1(Zero, wy105, :(Pos(Zero), wy2871)) → new_takeWhile1(Zero, Pos(Zero), wy2871)
new_takeWhile13(wy361, wy362, wy363, Succ(wy3640), Succ(wy3650)) → new_takeWhile13(wy361, wy362, wy363, wy3640, wy3650)
new_takeWhile12(Succ(wy23500), wy237, wy240) → new_takeWhile13(wy23500, Neg(Succ(wy237)), wy240, wy23500, wy237)
new_takeWhile1(Succ(wy500), wy105, :(Pos(Zero), wy2871)) → new_takeWhile11(wy500, Pos(Zero), wy2871)
new_takeWhile1(Zero, wy105, :(Neg(Zero), wy2871)) → new_takeWhile1(Zero, Neg(Zero), wy2871)
new_takeWhile1(Succ(wy500), wy105, :(Neg(Zero), wy2871)) → new_takeWhile13(wy500, Neg(Zero), wy2871, Succ(wy500), Zero)
new_takeWhile13(wy361, wy362, wy363, Succ(wy3640), Zero) → new_takeWhile11(wy361, wy362, wy363)
new_takeWhile11(wy500, wy186, wy185) → new_takeWhile1(Succ(wy500), wy186, wy185)
new_takeWhile14(wy500, wy186, wy185) → new_takeWhile1(Succ(wy500), wy186, wy185)
new_takeWhile1(wy50, wy105, :(Neg(Succ(wy287000)), wy2871)) → new_takeWhile12(wy50, wy287000, wy2871)
new_takeWhile1(wy50, wy105, :(Pos(Succ(wy287000)), wy2871)) → new_takeWhile10(wy50, wy287000, wy2871)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ DependencyGraphProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile19(wy155, :(Pos(Succ(wy265000)), wy2651)) → new_takeWhile16(Zero, wy265000, wy2651)
new_takeWhile19(wy155, :(Pos(Zero), wy2651)) → new_takeWhile19(Pos(Zero), wy2651)
new_takeWhile16(Succ(wy21800), wy220, wy223) → new_takeWhile15(wy21800, wy220, wy223, wy220, wy21800)
new_takeWhile18(wy155, wy264) → new_takeWhile19(wy155, wy264)
new_takeWhile15(wy349, wy350, :(Pos(Succ(wy351000)), wy3511), Succ(wy3520), Zero) → new_takeWhile16(Succ(wy349), wy351000, wy3511)
new_takeWhile15(wy349, wy350, wy351, Zero, Zero) → new_takeWhile17(wy349, wy350, wy351)
new_takeWhile16(Zero, wy220, wy223) → new_takeWhile18(Pos(Succ(wy220)), wy223)
new_takeWhile17(wy349, wy350, :(Pos(Succ(wy351000)), wy3511)) → new_takeWhile16(Succ(wy349), wy351000, wy3511)
new_takeWhile19(wy155, :(Neg(Zero), wy2651)) → new_takeWhile19(Neg(Zero), wy2651)
new_takeWhile15(wy349, wy350, wy351, Succ(wy3520), Succ(wy3530)) → new_takeWhile15(wy349, wy350, wy351, wy3520, wy3530)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
QDP
                          ↳ QDPSizeChangeProof
                        ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile16(Succ(wy21800), wy220, wy223) → new_takeWhile15(wy21800, wy220, wy223, wy220, wy21800)
new_takeWhile15(wy349, wy350, :(Pos(Succ(wy351000)), wy3511), Succ(wy3520), Zero) → new_takeWhile16(Succ(wy349), wy351000, wy3511)
new_takeWhile15(wy349, wy350, wy351, Zero, Zero) → new_takeWhile17(wy349, wy350, wy351)
new_takeWhile17(wy349, wy350, :(Pos(Succ(wy351000)), wy3511)) → new_takeWhile16(Succ(wy349), wy351000, wy3511)
new_takeWhile15(wy349, wy350, wy351, Succ(wy3520), Succ(wy3530)) → new_takeWhile15(wy349, wy350, wy351, wy3520, wy3530)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
QDP
                          ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile19(wy155, :(Pos(Zero), wy2651)) → new_takeWhile19(Pos(Zero), wy2651)
new_takeWhile19(wy155, :(Pos(Succ(wy265000)), wy2651)) → new_takeWhile16(Zero, wy265000, wy2651)
new_takeWhile18(wy155, wy264) → new_takeWhile19(wy155, wy264)
new_takeWhile16(Zero, wy220, wy223) → new_takeWhile18(Pos(Succ(wy220)), wy223)
new_takeWhile19(wy155, :(Neg(Zero), wy2651)) → new_takeWhile19(Neg(Zero), wy2651)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ DependencyGraphProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile110(Zero, wy21, wy138) → new_takeWhile(wy138)
new_takeWhile112(wy339, wy340, :(Neg(Succ(wy341000)), wy3411)) → new_takeWhile110(Succ(wy339), wy341000, wy3411)
new_takeWhile113(:(Neg(Zero), wy71)) → new_takeWhile113(wy71)
new_takeWhile113(:(Neg(Succ(wy7000)), wy71)) → new_takeWhile110(Zero, wy7000, wy71)
new_takeWhile111(wy339, wy340, :(Neg(Succ(wy341000)), wy3411), Zero, Succ(wy3430)) → new_takeWhile110(Succ(wy339), wy341000, wy3411)
new_takeWhile(:(Pos(Zero), wy71)) → new_takeWhile(wy71)
new_takeWhile111(wy339, wy340, wy341, Zero, Zero) → new_takeWhile112(wy339, wy340, wy341)
new_takeWhile111(wy339, wy340, wy341, Succ(wy3420), Succ(wy3430)) → new_takeWhile111(wy339, wy340, wy341, wy3420, wy3430)
new_takeWhile113(:(Pos(Zero), wy71)) → new_takeWhile(wy71)
new_takeWhile(:(Neg(Zero), wy71)) → new_takeWhile113(wy71)
new_takeWhile110(Succ(wy1900), wy21, wy138) → new_takeWhile111(wy1900, wy21, wy138, wy1900, wy21)
new_takeWhile(:(Neg(Succ(wy7000)), wy71)) → new_takeWhile110(Zero, wy7000, wy71)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
QDP
                          ↳ QDPSizeChangeProof
                        ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile110(Zero, wy21, wy138) → new_takeWhile(wy138)
new_takeWhile113(:(Neg(Zero), wy71)) → new_takeWhile113(wy71)
new_takeWhile113(:(Neg(Succ(wy7000)), wy71)) → new_takeWhile110(Zero, wy7000, wy71)
new_takeWhile(:(Pos(Zero), wy71)) → new_takeWhile(wy71)
new_takeWhile113(:(Pos(Zero), wy71)) → new_takeWhile(wy71)
new_takeWhile(:(Neg(Zero), wy71)) → new_takeWhile113(wy71)
new_takeWhile(:(Neg(Succ(wy7000)), wy71)) → new_takeWhile110(Zero, wy7000, wy71)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
QDP
                          ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile112(wy339, wy340, :(Neg(Succ(wy341000)), wy3411)) → new_takeWhile110(Succ(wy339), wy341000, wy3411)
new_takeWhile111(wy339, wy340, :(Neg(Succ(wy341000)), wy3411), Zero, Succ(wy3430)) → new_takeWhile110(Succ(wy339), wy341000, wy3411)
new_takeWhile111(wy339, wy340, wy341, Zero, Zero) → new_takeWhile112(wy339, wy340, wy341)
new_takeWhile111(wy339, wy340, wy341, Succ(wy3420), Succ(wy3430)) → new_takeWhile111(wy339, wy340, wy341, wy3420, wy3430)
new_takeWhile110(Succ(wy1900), wy21, wy138) → new_takeWhile111(wy1900, wy21, wy138, wy1900, wy21)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ DependencyGraphProof
                  ↳ QDP
                  ↳ QDP
              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile118(wy60, wy59) → new_takeWhile116(Zero, wy60, wy59)
new_takeWhile116(wy50, wy60, :(wy590, wy591)) → new_takeWhile117(wy50, wy590, wy591, wy590)
new_takeWhile117(Succ(wy500), wy60, wy59, Pos(Zero)) → new_takeWhile114(wy500, wy60, wy59, Zero, Succ(wy500))
new_takeWhile114(wy355, wy356, wy357, Zero, Zero) → new_takeWhile116(Succ(wy355), wy356, wy357)
new_takeWhile117(Zero, wy60, wy59, Pos(Zero)) → new_takeWhile116(Zero, wy60, wy59)
new_takeWhile117(Zero, wy60, wy59, Neg(Zero)) → new_takeWhile118(wy60, wy59)
new_takeWhile117(Succ(wy500), wy60, wy59, Neg(Zero)) → new_takeWhile115(Succ(wy500), wy60, wy59)
new_takeWhile114(wy355, wy356, wy357, Succ(wy3580), Succ(wy3590)) → new_takeWhile114(wy355, wy356, wy357, wy3580, wy3590)
new_takeWhile117(Succ(wy500), wy60, wy59, Pos(Succ(wy6200))) → new_takeWhile114(wy500, wy60, wy59, wy6200, wy500)
new_takeWhile117(wy50, wy60, :(wy590, wy591), Neg(Succ(wy6200))) → new_takeWhile117(wy50, wy590, wy591, wy590)
new_takeWhile115(wy50, wy60, :(wy590, wy591)) → new_takeWhile117(wy50, wy590, wy591, wy590)
new_takeWhile114(wy355, wy356, wy357, Zero, Succ(wy3590)) → new_takeWhile115(Succ(wy355), wy356, wy357)
new_takeWhile119(Succ(wy500), wy60, wy59, wy6200) → new_takeWhile114(wy500, wy60, wy59, wy6200, wy500)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
QDP
                        ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP
              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile117(Succ(wy500), wy60, wy59, Pos(Succ(wy6200))) → new_takeWhile114(wy500, wy60, wy59, wy6200, wy500)
new_takeWhile118(wy60, wy59) → new_takeWhile116(Zero, wy60, wy59)
new_takeWhile116(wy50, wy60, :(wy590, wy591)) → new_takeWhile117(wy50, wy590, wy591, wy590)
new_takeWhile117(wy50, wy60, :(wy590, wy591), Neg(Succ(wy6200))) → new_takeWhile117(wy50, wy590, wy591, wy590)
new_takeWhile117(Succ(wy500), wy60, wy59, Pos(Zero)) → new_takeWhile114(wy500, wy60, wy59, Zero, Succ(wy500))
new_takeWhile114(wy355, wy356, wy357, Zero, Zero) → new_takeWhile116(Succ(wy355), wy356, wy357)
new_takeWhile117(Zero, wy60, wy59, Neg(Zero)) → new_takeWhile118(wy60, wy59)
new_takeWhile117(Zero, wy60, wy59, Pos(Zero)) → new_takeWhile116(Zero, wy60, wy59)
new_takeWhile115(wy50, wy60, :(wy590, wy591)) → new_takeWhile117(wy50, wy590, wy591, wy590)
new_takeWhile117(Succ(wy500), wy60, wy59, Neg(Zero)) → new_takeWhile115(Succ(wy500), wy60, wy59)
new_takeWhile114(wy355, wy356, wy357, Zero, Succ(wy3590)) → new_takeWhile115(Succ(wy355), wy356, wy357)
new_takeWhile114(wy355, wy356, wy357, Succ(wy3580), Succ(wy3590)) → new_takeWhile114(wy355, wy356, wy357, wy3580, wy3590)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile120(wy235, wy236, wy237, Succ(wy2380), Succ(wy2390), wy240) → new_takeWhile120(wy235, wy236, wy237, wy2380, wy2390, wy240)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile121(wy218, wy219, wy220, Succ(wy2210), Succ(wy2220), wy223) → new_takeWhile121(wy218, wy219, wy220, wy2210, wy2220, wy223)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:


Haskell To QDPs